1. Field of the Invention
The present invention relates to a logic circuit equivalence verifying apparatus for verifying whether a plurality of logic circuits are logically equivalent to each other or not, and more particularly to an apparatus for verifying whether a behavioral description as an input to a behavioral synthesis system and a register transfer level description which is an output from the behavioral synthesis system are equivalent to each other or not.
2. Description of the Related Art
For designing LSI or VLSI circuits, it is general practice to employ an LSI design automation/support technology for automatizing or supporting the designing of LSI or VLSI circuits. One typical process of VLSI designing processes which employ the LSI design automation/support technology is a top-down design process using various EDA (electronic design automation) tools. The top-down design process is generally divided into a function design process, a logic design process, and a layout design process successively from its upstream step. Of these processes, automation of the function design process is referred to as behavioral synthesis (also high-level synthesis or functional synthesis), and automation of the logic design process is referred to as logic synthesis.
Specifically, according to the top-down design process, system specifications are produced by regarding an entire LSI circuit as a system and describing its behavior. The description thus generated is referred to as a behavioral description. The behavioral description is generating using a language like the C language, for example.
Then, in a behavioral synthesis phase, the generated behavioral description is automatically converted into an RTL (register transfer level) description. Heretofore, it has often been customary to manually perform the behavioral synthesis phase to generate an RTL description using an HDL (hardware description language).
Thereafter, in a logic synthesis phase, the RTL description is automatically converted into a gate level description (gate level logic circuit: net list). Based on the net list thus generated, a layout design process is carried out, followed by a chip design process.
Tools used to carry out the synthesis in each of the above synthesis phases are actually software-implemented. Since the tools are software-implemented, they are necessarily subject to bugs, and it is necessary to verify whether the synthesis in each of the above synthesis phases has been correct or not.
The logic synthesis phase has been performed relatively frequently, and hence the verification of the logic synthesis phase (logic verification) has also been performed frequently in order to prove the logic synthesis. However, the behavioral synthesis process has not been verified as much as the logic verification because it has often been replaced with a manual synthesis process.
To meet demands in recent years for LSI circuits which are more highly integrated and larger in scale, LSI circuits to be manufactured contain several million gates, which pose higher requirements for behavioral synthesis. In this connection, the verification of the behavioral synthesis phase is a very important task to be studied.
The conventionally most general form of the verification of the behavioral synthesis phase has been a simulation performed using a given test pattern. However, the simulation has suffered the following problems:
To carry out a simulation using a test pattern, the test pattern needs to be generated of necessity, and the generation of the test pattern is time-consuming and costly. The contents of a synthesis that can be verified by the simulation depend on the test pattern, and errors not considered by the test pattern that is used cannot be subject to the verification. Consequently, the conventional simulation-based verifying process may possibly produce unsatisfactory results.
Another process of verifying an RTL description generated from a behavioral description in the behavioral synthesis phase is carried out by verifying the equivalence between the RTL description and the behavioral description.
For example, an apparatus for verifying a behavioral synthesis is described in “Formal Methods in System Design”, Vol. 16, pp. 59–91, 2000 (document 1). The apparatus described in the document 1 outputs 1) a type specification description, 2) correctness lemmas, and 3) a verification script for a theorem proving system called PVS, from a behavioral description, an RTL description, and an associated relation which is a by-product of the behavioral synthesis. The correctness lemmas represent a logic formula which extracts an execution path (a series of states) for each basic block that does not contain a branch/confluence structure of a behavioral description and an RTL description, and when an associated relation of execution paths and an associated relation of signals are given, indicates that changes in signal values corresponding to the respective paths are the same. The theorem proving system PVS generates a function representing changes in signal values at the time the paths are executed, according to a verification script using a term rewriting system. It is checked if functions indicating changes in a corresponding signal pair in corresponding paths are equivalent. If functions indicating changes in pairs of all corresponding paths and pairs of all corresponding signal values are equivalent, then the behavioral description and the RTL description are equivalent to each other.
Another apparatus for verifying a behavioral synthesis is described in “International Conference on Computer Design”, pp. 458–466, 1999 (document 2). The apparatus described in the document 2 is the same as the apparatus described in the document 1 in that it extracts an execution path, and when an associated relation of execution paths and an associated relation of signals are given, it generates functions indicating changes in signal values at the time respective paths are executed, and checks if functions for corresponding signals in corresponding paths are equivalent. In the apparatus described in the document 2, however, extracted execution paths are not limited to basic blocks. The apparatus extracts execution paths while developing a repetitive structure (looped structure) of an original behavioral description until an execution path corresponding to the RTL description is found. Functions indicative of changes in signal values are generated using a technique called a symbol simulation, rather than the term rewriting system.
The conventional verifying apparatus disclosed in the documents 1 and 2 have the following problems:
The first problem is that they do not handle the verification of complete equivalence between a behavioral description and an RTL description for the reason that the steps carried out in the behavioral synthesis process are limited to only scheduling and binding. Generally, the behavioral synthesis process carries out not only these steps, but also a preprocessing step for converting a received behavioral description into a form suitable for subsequent steps and a postprocessing step for converting a description subjected to binding into an RTL description capable of being logically synthesized. However, since there is a large separation of abstractness between a behavioral description and an RTL description, it is difficult to verify, at one time, complete equivalence between a behavioral description and an RTL description including those steps.
The second problem is that the verification is time-consuming for the following reason: According to the above documents 1, 2, when a description includes a control structure, paths (execution series) free of confluences are extracted, and changes in signal values in the respective paths are extracted and compared. Since the number of execution series increases exponentially depending on the number of branch/confluence structures, if the control structure is complex, then the number of paths increases, and the number of symbol simulations and the number of times that function values are compared also increase, resulting in a longer time required for the verification.